So foil is one way of doing inductive logic programming and the idea is you basically

start by covering the positive examples by very simple head, one head prologue programs

and adding body literals and additional clauses, essentially in an and or tree that prologue

programs give you.

And that works if you can solve the problems of how to choose literals and which are good

literals.

This is restricted to the original language that came with the problem.

There's another way, there's these two dominant things in inductive logic program.

The other one is called inverse resolution.

So the idea is that if you have the background knowledge, you have a hypothesis and you have

the descriptions, then that actually entails the classifications.

That was one of the major tenets we had in the beginning.

So if we know that we have an entailment, we can prove it and we can write it down

in logic, then we can actually prove it via resolution.

So the idea here is instead of like yesterday taking the same proof as an explanation and

running it again, which is essentially doing two things at the same time, what we can also

do is just basically run the proof backwards.

The nicer thing about running a proof backwards is that we always know in resolution at least

where to start at, namely at the empty clause.

So what you want to do is you just basically literally want to do the resolution backwards.

So in normal resolution, you have two clauses, one of the form L or some rest and another

one not L, where L is a literal some other rest and you get a resolvent R1 or R2.

So for running things backwards, you can do two things.

Either you start out with C and produce C1 and C2, or you take C and C1 and produce C2.

The second one, of course, is much more guided.

Let us look at an example.

And I've taken the liberty to write clauses as implications.

That makes sense for horn clauses.

So we run a resolution proof backwards.

We've turned out one thing you see is normally you see a resolution proof that basically

says, take this, take that, make something new.

The arrow is pointing downwards, here you can see they're pointing upwards.

So we'll start out with the empty clause, which is essentially to implies false.

And then we have an example which we write down as a horn clause as well and say, well,

grandparent of George and Anne is false.

We have a negative example here and we resolve that with, we can resolve, we can find out

if this clause is supposed to give an empty clause with a resolution partner, this must

be a unit clause as well, namely not grandparent of George and Anne, which I write here as

true implies grandparent of George and Anne.

Now what we can do, once we can do, again, we have another example.

Elizabeth and Anne are a positive example.

So Elizabeth is a grandparent, no, is a positive example for parent, one of our facts, and

we can resolve that here with not parent Elizabeth Y and grandparent George Y using the substitution

Anne for Y.

And then we can do it again if we have a clause here with parent Elizabeth Y implies grandparent

of Y, then which we've probably gotten somewhere like this, then we can get this clause, parent

F X Y implies parent of Z Y implies grandparent of X Y.

There is something wrong here.

Who can spot this?

It should be parent, that should be a Z.